package edu.luc.cs.trull.translator;

// TODO GEORGE update this for Trull, consider porting to XSLT or XStream

import java.io.*;

import org.w3c.dom.*;
import java.util.*;
import javax.xml.parsers.DocumentBuilderFactory;
import org.apache.log4j.*;

/**
 * An XML front end for Trull.
 */
public class Translator implements Visitor {

    private static Logger cat = Logger.getLogger(Translator.class.getName());

    /** Print writer. */
    private PrintWriter out;

    /** the number of tabs for indentation */
    private int numOfTabs = 0;

    /**
     * A visitor for a data node.
     */
    private interface DataVisitor {
        void visitData(Node node);
    }

    /**
     * A visitor for an ActionComponent.
     */
    class ActionExprVisitor implements DataVisitor {
        public void visitData(Node node){
            int savedTabs = numOfTabs;
            out.print("new Init(new ActionComponent(){");
            numOfTabs++;
            newIndentedLine();
            out.print("public void execute(final LabeledEvent event){");
            numOfTabs++;
            newIndentedLine();

            visit(node);

            numOfTabs = savedTabs;
            newIndentedLine();
            out.print("}})/*Init*/");
        }
    }

    //
    // Constructors
    //

    /** Default constructor. */
    public Translator(PrintWriter out) { this.out = out; }

    //
    // Public static methods
    //

    /** Parses the resulting document tree. */
    public static void visit(String uri, PrintWriter out) {

        try {
            Document document = DocumentBuilderFactory.newInstance().newDocumentBuilder().parse(uri);
            new Translator(out).visit(document);
        }
        catch (Exception e) {
            cat.error("parse exception", e);
        }

    } // parse(String, String)

    public static void main(String[] argv) {

        BasicConfigurator.configure();
        Logger.getRootLogger().setLevel(Level.INFO);
        cat.setLevel(Level.INFO);

        // is there anything to do?
        if (argv.length != 1 && argv.length != 2) {
            printUsage();
            System.exit(1);
        }

        PrintWriter out = null;

        try {
            if (argv.length == 2) {
                cat.info("creating file " + argv[1]);
                out = new PrintWriter(new OutputStreamWriter(new FileOutputStream(argv[1]), "UTF8"));
            } else {
                out = new PrintWriter(new OutputStreamWriter(System.out, "UTF8"));
            }
        } catch (Throwable e) {
            cat.warn("problem creating output writer", e);
        }

        // process uri
        cat.info("processing " + argv[0]);
        visit(argv[0], out);

        if (argv.length == 2) {
            out.close();
        }

    } // main(String[])

    /** Prints the usage. */
    private static void printUsage() {

        System.err.println("usage: java triveni.xml.Translator uri [ output-file ]");

    } // printUsage()

    public void visit(Node node){

        if (node == null) {
            return;
        }

        int type = node.getNodeType();

        switch (type) {
            // traverse document
            case Node.DOCUMENT_NODE: {
                visit(((Document)node).getDocumentElement());
                out.flush();
                break;
            }

            // traverse element using visitor
            case Node.ELEMENT_NODE: {
                dispatch(node);
                break;
            }

            // handle entity reference nodes
            case Node.ENTITY_REFERENCE_NODE: {
                visitChildren(node);
                break;
            }

            // print text
            case Node.CDATA_SECTION_NODE:
            case Node.TEXT_NODE: {
                //such node begins without printing new line
                String str = node.getNodeValue();
                if(str.trim().length() == 0) break;
                int savedTabs = numOfTabs;

                int indent = countSpace(str);
                StringTokenizer st = new StringTokenizer(str.trim(), "\n");
                //first line doesn't start with a new line
                if(st.hasMoreTokens()){
                    String first = st.nextToken();
                    out.print(first.trim());
                }
                while(st.hasMoreTokens()){
                    String next = st.nextToken();
                    int actual = countSpace(next);
                    int needed = indent < actual ? actual - indent : 0;
                    newIndentedLine();
                    for(int i = 0; i < needed; i++) out.print(" ");
                    out.print(next.trim());
                }
                break;
            }

            default: {

        // ignore

                cat.info("ignoring node of type " + type + ": " + node);
                break;
            }
        }
    }

    private int countSpace(String str){
        int count = 0;
        boolean done = false;
        for(int i = 0; (!done) && i < str.length(); i++){
            switch(str.charAt(i)){
            case '\t':
                count = (count/8 + 1) * 8;
                break;
            case ' ':
                count++;
                break;
            case '\n':
                break;
            default:
                done = true;
            }
        }
        return count;
    }

    /**
     * Invokes the method corresponding to the current element name.
     * Add more cases here as elements are added in triveni.dtd and create
     * the corresponding traversal methods.
     */

    void dispatch(Node node) {
        String name = node.getNodeName();
        Visitor visitor = this;
        if (ACT.equals(name)) { visitor.act(node);
        } else if (ACTIVITY.equals(name)) { visitor.activity(node);
        } else if (ACTIVITYREF.equals(name)) { visitor.activityRef(node);
        } else if (ASSERT.equals(name)) { visitor.assertt(node);
        } else if (ASSERTION.equals(name)) { visitor.assertion(node);
        } else if (AWAIT.equals(name)) { visitor.await(node);
        } else if (AWAITONE.equals(name)) { visitor.awaitOne(node);
        } else if (CASE.equals(name)) { visitor.cse(node);
        } else if (CODE.equals(name)) { visitor.code(node);
        } else if (CONTROLLABLE.equals(name)) { visitor.controllable(node);
        } else if (DECLARE.equals(name)) { visitor.declare(node);
        } else if (DEFAULT.equals(name)) { visitor.defult(node);
        } else if (DONE.equals(name)) { visitor.done(node);
        } else if (EMIT.equals(name)) { visitor.emit(node);
        } else if (EVENTLABEL.equals(name)) { visitor.eventLabel(node);
        } else if (EVENTLABELS.equals(name)) { visitor.eventLabels(node);
        } else if (EXPR.equals(name)) { visitor.expr(node);
        } else if (EXPRREF.equals(name)) { visitor.exprRef(node);
        } else if (EXPRSREF.equals(name)) { visitor.exprsRef(node);
        } else if (IF.equals(name)) { visitor.iif(node);
        } else if (IMPORT.equals(name)) { visitor.imprt(node);
        } else if (LOCAL.equals(name)) { visitor.local(node);
        } else if (LOOP.equals(name)) { visitor.loop(node);
        } else if (NIL.equals(name)) { visitor.nil(node);
        } else if (ONEMIT.equals(name)) { visitor.onEmit(node);
        } else if (ONRESUME.equals(name)) { visitor.onResume(node);
        } else if (ONSTART.equals(name)) { visitor.onStart(node);
        } else if (ONSTOP.equals(name)) { visitor.onStop(node);
        } else if (ONSUSPEND.equals(name)) { visitor.onSuspend(node);
        } else if (PARALLEL.equals(name)) { visitor.parallel(node);
        } else if (PARAM.equals(name)) { visitor.param(node);
        } else if (PREDICATE.equals(name)) { visitor.predicate(node);
        } else if (RENAME.equals(name)) { visitor.rename(node);
        } else if (RETURN.equals(name)) { visitor.retrn(node);
        } else if (RUN.equals(name)) { visitor.run(node);
        } else if (SATISFIED.equals(name)) { visitor.satisfied(node);
        } else if (SEQUENCE.equals(name)) { visitor.sequence(node);
        } else if (SUSPENDRESUME.equals(name)) { visitor.suspendResume(node);
        } else if (SWITCH.equals(name)) { visitor.swtch(node);
        } else if (THREADACTIVITY.equals(name)) { visitor.threadActivity(node);
        } else if (TIMEOUT.equals(name)) { visitor.timeOut(node);
        } else if (TRIVENI.equals(name)) { visitor.triveni(node);
        } else if (UPDATE.equals(name)) { visitor.update(node);
        } else if (UPDATEHANDLER.equals(name)) { visitor.updateHandler(node);
        } else if (VALUATOR.equals(name)) { visitor.valuator(node);
        } else if (VIOLATED.equals(name)) { visitor.violated(node);
        } else if (WATCHING.equals(name)) { visitor.watching(node);
        } else if (ALLPAST.equals(name)) { visitor.allPast(node);
        } else if (AND.equals(name)) { visitor.and(node);
        } else if (BACKTO.equals(name)) { visitor.backTo(node);
        } else if (IMPLIES.equals(name)) { visitor.implies(node);
        } else if (LABEL.equals(name)) { visitor.label(node);
        } else if (LEAF.equals(name)) { visitor.leaf(node);
        } else if (NOT.equals(name)) { visitor.not(node);
        } else if (ONCE.equals(name)) { visitor.once(node);
        } else if (OR.equals(name)) { visitor.or(node);
        } else if (PREVIOUS.equals(name)) { visitor.previous(node);
        } else if (SINCE.equals(name)) { visitor.since(node);
        } else {
            cat.error("Unknown element " + name);
        }
    }

    //<!ELEMENT ACT             (%activity;)				>

    public void act(Node node){
        out.print("new Act(");
        visitUntilNamedChild(node, ACTIVITIES, null);
        out.print(")/*Act*/");
    }

    //<!ELEMENT ACTIVITY	(DECLARE?, CODE?, UPDATEHANDLER?,
    //                           (UPDATE | ONEMIT | ONRESUME | ONSUSPEND
    //				  | ONSTART | ONSTOP)* )                >
    //<!ATTLIST ACTIVITY
    //            NAME		ID	              #IMPLIED
    //            ACCESS        (public | package)    "public"
    //            EXTENDS       NMTOKEN     #FIXED    "Activity"
    //	          IMPLEMENTS	NMTOKENS	      #IMPLIED
    //	          PARAMS	CDATA		      #IMPLIED          >

    public void activity(Node node){
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);

        int savedTabs = numOfTabs;

        validateDeclarables(node);
        validateClassHeader(node);

        if(name != null){
            newIndentedLine();
            classHeader(attrs);
            out.print("{");
        } else out.print("new Activity(){");

        numOfTabs++;
        activityBody(node);

        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}/*Activity*/");
    }//activity

    //<!ELEMENT ACTVITYREF	      (PARAM)*                          >
    //<!--         NAME               Name of the referenced activity -->
    //<!ATTLIST ACTIVITYREF
    //             NAME               NMTOKEN                #REQUIRED
    //	           TYPE		      (Class | Object)       "Class"    >

    public void activityRef(Node node){
        String type = node.getAttributes().getNamedItem(TYPE).getNodeValue();
        Node actName = node.getAttributes().getNamedItem(NAME);
        if("Class".equals(type)){
            out.print("new ");
            out.print(actName.getNodeValue() + "(");
            visitWhileNamedChild(node, PARAM, null, ", ", 0);
            out.print(")");
        } else out.print(actName.getNodeValue());
    }//activityRef


    //<!ELEMENT ASSERT		 (%tlexpr;)				 >
    //<!ATTLIST ASSERT
    //            NAME           NMTOKEN                     "Assertion" >

    public void assertt(Node node){
        out.print("new Assert(\"");
        signature(node.getAttributes().getNamedItem(NAME));
        out.print("\", ");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        visitUntilNamedChild(node, TLEXPRS, null);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*Assert*/");
    }//assert

    //<!ELEMENT ASSERTION             (%tlexpr;)		                >

    public void assertion(Node node){
        out.print("new Assertion(");
        visitUntilNamedChild(node, TLEXPRS, null);
        out.print(")/*Assertion*/");
    }//assert

    //<!ELEMENT AWAIT		(#PCDATA | (%expr;))*			>
    //<!ATTLIST AWAIT		%signatures;                            >
    //<!ENTITY %  signatures	"SIGNATURE IDREFS            #REQUIRED" >

    public void await(Node node){
        int savedTabs = numOfTabs;
        out.print("new Await(");
        signatures(node.getAttributes().getNamedItem(SIGNATURE));
        if(node.hasChildNodes()){
            out.print(", ");
            sequence(node);
        }
        out.print(")/*Await*/");
    }//await

    //<!ELEMENT AWAITONE	(CASE+)                                 >

    public void awaitOne(Node node){
        out.println("new AwaitOne(new Case[]{");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        visitWhileNamedChild(node, CASE, null, ", ", 2);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("})/*AwaitOne*/");
    }//awaitOne

    //<!ELEMENT CASE            (#PCDATA | (%expr;))*			>
    //<!ATTLIST CASE		%signature;                             >

    public void cse(Node node){
        int savedTabs = numOfTabs;
        out.print("new Case(");
        signature(node.getAttributes().getNamedItem(SIGNATURE));
        if(node.hasChildNodes()){
            out.print(", ");
            sequence(node);
        }
        out.print(")/*Case*/");
    }//cse

    //<!ELEMENT CODE	                (#PCDATA)                      >

    public void code(Node node){
        newIndentedLine();
        visitChildren(node);
    }//code

    // <!ELEMENT CONTROLLABLE    (DECLARE?, CODE?, %expr;)            >
    // <!ATTLIST CONTROLLABLE
    //             NAME         ID                     #IMPLIED
    //	           ACCESS	(public | package)     "public"
    //             EXTENDS      NMTOKEN    #FIXED      "triveni.Controllable"
    //             IMPLEMENTS   NMTOKENS               #IMPLIED
    //             PARAMS       NMTOKENS               #IMPLIED      >

    public void controllable(Node node){
        generalExpr(node);
    }//controllable

    //<!ELEMENT DECLARE		        (#PCDATA | %decl; | EVENTLABEL)* >

    public void declare(Node node){
        String[] ALL_DECLARABLES = new String[DECLARABLES.length + 1];
        for(int i = 0; i < DECLARABLES.length; i++)
            ALL_DECLARABLES[i] = DECLARABLES[i];
        ALL_DECLARABLES[DECLARABLES.length] = EVENTLABEL;
        newIndentedLine();
        visitWhileNamedChild(node, ALL_DECLARABLES, new DataVisitor(){
                public void visitData(Node node){
                    newIndentedLine();
                    visit(node);
                }
            }, "", 1);
    }//declare

    //<!ELEMENT DEFAULT          (#PCDATA | %expr;)*                     >

    public void defult(Node node){
        sequence(node);
    }//defult

    //<!ELEMENT DONE             EMPTY                                   >

    public void done(Node node){
        out.print("new Done()");
    }//done

    //<!ELEMENT EMIT		(DECLARE?, CODE?, RETURN?)              >
    //<!ATTLIST EMIT		%signature;				>

    public void emit(Node node){
        out.print("new Emit(");
        signature(node.getAttributes().getNamedItem(SIGNATURE));
        if(node.hasChildNodes()){
            out.print(", new Emitter(){");
            int savedTabs = numOfTabs++;
            if(hasNamedChild(node, DECLARE)){
                newIndentedLine();
                visitUntilNamedChild(node, DECLARE, null);
            }
            newIndentedLine();
            out.print("public Object execute(final LabeledEvent event){");
            numOfTabs++;
            if(hasNamedChild(node, CODE)){
                newIndentedLine();
                visitUntilNamedChild(node, CODE, null);
            }
            if(hasNamedChild(node, RETURN)){
                newIndentedLine();
                visitUntilNamedChild(node, RETURN, null);
            }
            numOfTabs = savedTabs;
            newIndentedLine();
            out.print("}}");
        }
        out.print(")");
    }//emit

    //<!ELEMENT EVENTLABEL		EMPTY                          >
    //<!ATTLIST EVENTLABEL NAME         ID                   #REQUIRED >

    public void eventLabel(Node node){
        out.print("public static final String ");
        out.print(node.getAttributes().getNamedItem(NAME).getNodeValue());
        out.print(" = \"");
        out.print(node.getAttributes().getNamedItem(NAME).getNodeValue());
        out.print("\";");
    }//eventLabel

    //<!ELEMENT EVENTLABELS		(EVENTLABEL)*                         >
    //<!ATTLIST EVENTLABELS NAME      ID                            #REQUIRED >

    public void eventLabels(Node node){
        newIndentedLine();
        out.print("interface ");
        NamedNodeMap attrs = node.getAttributes();
        Node className = attrs.getNamedItem(NAME);
        out.println(className.getNodeValue() + "{");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        visitWhileNamedChild(node, EVENTLABEL, null, ";", 1);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.println("}");
    }//eventLabels

    // <!ELEMENT EXPR           (DECLARE?, CODE?, %expr;)            >
    // <!ATTLIST EXPR
    //             NAME         ID                     #IMPLIED
    //	           ACCESS	(public | package)     "public"
    //             EXTENDS      NMTOKEN    #FIXED      "triveni.Expr"
    //             IMPLEMENTS   NMTOKENS               #IMPLIED
    //             PARAMS       NMTOKENS               #IMPLIED      >

    public void expr(Node node){
        generalExpr(node);
    }//expr

    //<!ELEMENT EXPRREF		(PARAM)*                                >
    //<!--         NAME         Name of the referenced expr     -->
    //<!ATTLIST EXPRREF
    //             NAME		NMTOKEN               #REQUIRED
    //	           TYPE		(Class | Object)      "Class"           >

    public void exprRef(Node node){
        Node exprName = node.getAttributes().getNamedItem(NAME);
        String type = node.getAttributes().getNamedItem(TYPE).getNodeValue();
        if("Class".equals(type)){
            out.print("new ");
            out.print(exprName.getNodeValue() + "(");
            visitWhileNamedChild(node, PARAM, null, ", ", 0);
            out.print(")");
        } else out.print(exprName.getNodeValue());
    }//exprRef


    //<!ELEMENT EXPRSREF	EMPTY                                   >
    //<!ATTLIST EXPRSREF
    //             NAME         NMTOKEN                       #REQUIRED >

    public void exprsRef(Node node){
        out.print(node.getAttributes().getNamedItem(NAME).getNodeValue());
    }

    //<!ELEMENT IF               (PREDICATE, SATISFIED, VIOLATED?)       >

    public void iif(Node node){
        int savedTabs = numOfTabs;
        out.print("new If(");
        visitUntilNamedChild(node, PREDICATE, null);
        out.print(",");
        newIndentedLine();
        visitUntilNamedChild(node, SATISFIED, null);
        if(hasNamedChild(node, VIOLATED)){
            out.print(",");
            newIndentedLine();
            visitUntilNamedChild(node, VIOLATED, null);
        }
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*If*/");
    }//iif

    //<!--		       Import			             -->
    //<!--		       Import statements in the host language-->
    //<!ELEMENT IMPORT		        (#PCDATA)                      >

    public void imprt(Node node){
        visitChildren(node);
    }//imprt

    //<!ELEMENT LOCAL	        (#PCDATA | %expr;)*			>
    //<!ATTLIST LOCAL		%signatures;				>

    public void local(Node node){
        out.print("new Local(");
        signatures(node.getAttributes().getNamedItem(SIGNATURE));
        out.print(", ");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        sequence(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*Local*/");
    }//local

    //<!ELEMENT LOOP		(#PCDATA | %expr;)*		        >

    public void loop(Node node){
        out.print("new Loop(");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        sequence(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*Loop*/");
    }//loop

    //<!ELEMENT NIL              EMPTY				         >

    public void nil(Node node){
        out.print("new Nil()");
    }//nil

    //<!ELEMENT ONEMIT                (#PCDATA)                         >

    public void onEmit(Node node){
        callBack(node, "onEmit");
    }//onEmit

    //<!ELEMENT ONRESUME		(#PCDATA)			>

    public void onResume(Node node){
        callBack(node, "onResume");
    }//onResume

    //<!ELEMENT ONSTART		       (#PCDATA)			>

    public void onStart(Node node){
        callBack(node, "onStart");
    }//onStart

    //<!ELEMENT ONSTOP		        (#PCDATA)			>

    public void onStop(Node node){
        callBack(node, "onStop");
    }//onStop

    //<!ELEMENT ONSUSPEND		(#PCDATA)		       >

    public void onSuspend(Node node){
        callBack(node, "onSuspend");
    }//onSuspend

    //<!ELEMENT PARALLEL	(EXPRSREF | (%expr;)+)			       >

    public void parallel(Node node){
        int savedTabs = numOfTabs++;
        out.print("new Parallel(");
        if(!hasNamedChild(node, EXPRSREF)) {
            out.print("new Expr[]{");
            newIndentedLine();
            visitWhileNamedChild(node, EXPRS, null, ", ", 2);
            out.print("}");
        } else {
            visitUntilNamedChild(node, EXPRSREF, null);
        }
        out.print(")/*Parallel*/");
    }//parallel

    //<!ELEMENT PARAM          (#PCDATA)                              >
    public void param(Node node){
        visitChildren(node);
    }//param

    //<!ATTLIST ---- PARAMS    CDATA                                  >
    public void params(Node node){
        out.print(node.getNodeValue());
    }//params

    //<!ELEMENT PREDICATE	 (DECLARE?, CODE?, RETURN)            >

    public void predicate(Node node){
        out.print("new Predicate(){");
        numOfTabs++;
        if(hasNamedChild(node, DECLARE)){
            newIndentedLine();
            visitUntilNamedChild(node, DECLARE, null);
        }
        newIndentedLine();
        out.print("public boolean execute(final LabeledEvent event){");
        int savedTabs = numOfTabs++;
        if(hasNamedChild(node, CODE)){
            newIndentedLine();
            visitUntilNamedChild(node, CODE, null);
        }
        newIndentedLine();
        visitUntilNamedChild(node, RETURN, null);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}}");
    }//predicate

    //<!ELEMENT RENAME		(#PCDATA | %expr;)*		        >
    //<!ATTLIST RENAME
    //            FROM          (IDREF|IDREFS)              #REQUIRED
    //	          TO            (IDREF|IDREFS)              #REQUIRED   >

    public void rename(Node node){
        out.print("new Rename(");
        signatures(node.getAttributes().getNamedItem(FROM));
        out.print(", ");
        signatures(node.getAttributes().getNamedItem(TO));
        out.print(", ");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        sequence(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*Rename*/");
    }//rename

    //<!ELEMENT RETURN	                (#PCDATA)                      >

    public void retrn(Node node){
        out.print("return ");
        visitChildren(node);
        out.print(";");
    }//retrn

    //<!ELEMENT RUN			(#PCDATA)                                 >
    public void run(Node node){
        int savedTabs = numOfTabs;
        out.print("public void run(){");
        numOfTabs++;
        newIndentedLine();
        visitChildren(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}");
    }

    //<!ELEMENT SATISFIED	 (#PCDATA | %expr;)*                    >

    public void satisfied(Node node){
        sequence(node);
    }//satisfied

    //<!ELEMENT SEQUENCE	(#PCDATA | %expr;)*			>

    public void sequence(Node node){
        switch(numOfNonEmptyChildren(node)){
        case 0: done(node); break;
        case 1:
            visitUntilNamedChild(node, EXPRS, new ActionExprVisitor());
            break;
        default:
            out.print("new Sequence(new Expr[]{");
            int savedTabs = numOfTabs++;
            newIndentedLine();
            visitWhileNamedChild(node, EXPRS, new ActionExprVisitor(), ", ", 2);
            numOfTabs = savedTabs;
            newIndentedLine();
            out.print("})/*Sequence*/");
        }
    }//sequence

    //<!ENTITY %  signature	 "SIGNATURE IDREF             #REQUIRED">
    public void signature(Node node){
        out.print(node.getNodeValue());
    }//signature

    //<!ENTITY %  signatures	 "SIGNATURE IDREFS            #REQUIRED">
    public void signatures(Node node){
        StringTokenizer params = new StringTokenizer(node.getNodeValue());
        out.print("new String[]{");
        if (params.hasMoreElements()) {
            out.print(params.nextElement());
        }
        while (params.hasMoreElements()) {
            out.print(", " + params.nextElement());
        }
        out.print("}");
    }//signatures

    //<!ELEMENT SUSPENDRESUME	 (#PCDATA | %expr;)*                     >
    //<!ATTLIST SUSPENDRESUME
    //              SUSPEND      NMTOKENS                     #REQUIRED
    //	            RESUME       NMTOKENS                     #REQUIRED  >

    public void suspendResume(Node node){
        out.print("new SuspendResume(");
        signatures(node.getAttributes().getNamedItem(SUSPEND));
        out.print(", ");
        signatures(node.getAttributes().getNamedItem(RESUME));
        out.print(", ");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        sequence(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*SuspendResume*/");
    }//suspendResume

    //<!ELEMENT SWITCH            (VALUATOR, (%expr;)+, DEFAULT?)         >

    public void swtch(Node node){
        int savedTabs = numOfTabs;
        out.print("new Switch(");
        visitUntilNamedChild(node, VALUATOR, null);
        out.print(", new Expr[]{");
        numOfTabs++;
        newIndentedLine();
        visitWhileNotNamedChild(node, DEFAULT, null, ",", 2);
        numOfTabs--;
        newIndentedLine();
        out.print("}");
        if(hasNamedChild(node, DEFAULT)){
            out.print(", ");
            newIndentedLine();
            visitUntilNamedChild(node, DEFAULT, null);
        }
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")/*Switch*/");
    }//swtch

    //<!ELEMENT THREADACTIVITY        (DECLARE?, CODE?, UPDATEHANDLER?,
    //                                 (UPDATE | ONEMIT | ONRESUME | ONSUSPEND
    //				        | ONSTART | ONSTOP)*, RUN )     >
    //<!ATTLIST THREADACTIVITY
    //            NAME		ID	              #IMPLIED
    //	          ACCESS	(public | package)    "public"
    //	          EXTENDS       NMTOKEN      #FIXED   "ThreadActivity"
    //	          IMPLEMENTS	NMTOKENS	      #IMPLIED
    //	          PARAMS	CDATA		      #IMPLIED          >

    public void threadActivity(Node node){
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);

        int savedTabs = numOfTabs;

        validateDeclarables(node);
        validateClassHeader(node);

        if(name != null){
            newIndentedLine();
            classHeader(attrs);
            out.print("{");
        } else out.print("new ThreadActivity(){");

        numOfTabs++;
        activityBody(node);

        newIndentedLine();
        visitUntilNamedChild(node, RUN, null);

        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}");
    }

    //<!ELEMENT TIMEOUT               (#PCDATA | (%expr;))*               >
    public void timeOut(Node node){
        sequence(node);
    }

    //<!ELEMENT TRIVENI                (IMPORT?, (%decl;)+)		        >
    //<!ATTLIST TRIVENI
    //	            PACKAGE             NMTOKEN               #IMPLIED          >

    public void triveni(Node node){
        out.println("/**** IMPORTANT : AUTOMATICALLY GENERATED. DON'T EDIT! ****/");
        NamedNodeMap attrs = node.getAttributes();

        //package declaration
        Node pkg = attrs.getNamedItem(PACKAGE);
        if (pkg != null){
            out.println("package " + pkg.getNodeValue() + ";");
            out.println("");
        }

        //default imports
        out.println("import triveni.*;");
        out.println("import triveni.tl.*;");
        out.println("import triveni.Expr;");

        //user imports
        visitUntilNamedChild(node, IMPORT, null);
        out.println("");
        out.println("");

        visitWhileNamedChild(node, DECLARABLES, null, "", 2);
    }

    //<!ELEMENT UPDATE                (#PCDATA)	                       >

    public void update(Node node){
        int savedTabs = numOfTabs;
        newIndentedLine();
        out.print("public void update(final LabeledEvent event){");
        numOfTabs++;
        newIndentedLine();
        visitChildren(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}");
    }

    //<!ELEMENT UPDATEHANDLER         (#PCDATA | %expr;)*	       >

    public void updateHandler(Node node){
        sequence(node);
    }

    //<!ELEMENT VALUATOR         (DECLARE?, CODE?, RETURN)               >

    public void valuator(Node node){
        out.print("new Valuator(){");
        numOfTabs++;
        if(hasNamedChild(node, DECLARE)){
            newIndentedLine();
            visitUntilNamedChild(node, DECLARE, null);
        }
        newIndentedLine();
        out.print("public int execute(final LabeledEvent event){");
        int savedTabs = numOfTabs++;
        if(hasNamedChild(node, CODE)){
            newIndentedLine();
            visitUntilNamedChild(node, CODE, null);
        }
        newIndentedLine();
        visitUntilNamedChild(node, RETURN, null);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}}/*Valuator*/");
    }//valuator

    //<!ELEMENT VIOLATED	 (#PCDATA | %expr;)*                    >

    public void violated(Node node){
        sequence(node);
    }//violated

    //<!ELEMENT WATCHING	((%expr;), (TIMEOUT | CASE+)?)	        >
    //<!ATTLIST WATCHING	%signatures;	                        >

    public void watching(Node node){
        out.print("new Watching(");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        visitUntilNamedChild(node, EXPRS, null);
        out.print(", ");
        numOfTabs = savedTabs + 1;
        if(!hasNamedChild(node, CASE)){
            signatures(node.getAttributes().getNamedItem(SIGNATURE));
        }
        if(hasNamedChild(node, TIMEOUT)){
            out.print(", ");
            newIndentedLine();
            visitUntilNamedChild(node, TIMEOUT, null);
        }else if(hasNamedChild(node, CASE)){
            numOfTabs = savedTabs + 1;
            newIndentedLine();
            out.print("new Case[]{");
            numOfTabs = savedTabs + 2;
            newIndentedLine();
            visitWhileNamedChild(node, CASE, null, ", ", 2);
            numOfTabs = savedTabs + 1;
            newIndentedLine();
            out.print("}");
        }
        out.print(")/*Watching*/");
    }//watching



    //
    //some private method for visiting exprs
    //


    //a general visitor for exprs, includes triveni.Expr and triveni.Controllable

    private void generalExpr(Node node){
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);
        Node params = attrs.getNamedItem(PARAMS);
        Node extnds = attrs.getNamedItem(EXTENDS);

        int savedTabs = numOfTabs;

        validateDeclarables(node);
        validateClassHeader(node);

        if(name != null){
            newIndentedLine();
            classHeader(attrs);
            out.print("{");
        } else out.print("new " + extnds.getNodeValue() + "(){");


        //add parameters as instance fields
        if((name != null) && (params != null)){
            numOfTabs = savedTabs + 1;
            paramsAsInstanceFields(params);
        }

        //class member declaration
        if(hasNamedChild(node, DECLARE)){
            numOfTabs = savedTabs + 1;
            visitUntilNamedChild(node, DECLARE, null);
        }
        out.println("");

        //constructor declaration

        numOfTabs = savedTabs + 1;
        newIndentedLine();
        if(name != null) constructorHeader(attrs);
        out.print("{");

        if((name != null) && (params != null)){
            numOfTabs = savedTabs + 2;
            initializeParamsInstanceFields(params);
        }

        if(hasNamedChild(node, CODE)){
            numOfTabs = savedTabs + 2;
            visitUntilNamedChild(node, CODE, null);
        }
        out.println("");

        numOfTabs = savedTabs + 2;
        newIndentedLine();
        out.print("become(");

        //the expr
        visitUntilNamedChild(node, EXPRS, null);

        out.print(");");

        numOfTabs = savedTabs + 1;
        newIndentedLine();
        out.println("}");
        out.println("");
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}");
    }//generalExpr

    //the body of an Activity or ThreadActivity

    private void activityBody(Node node){
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);
        Node params = attrs.getNamedItem(PARAMS);

        int savedTabs = numOfTabs;

        validateActivityBody(node);

        if((name != null) && (params != null)) paramsAsInstanceFields(params);

        //class member declaration
        if(hasNamedChild(node, DECLARE)) visitUntilNamedChild(node, DECLARE, null);
        out.println("");

        //need a constructor if the the class has a name, or it is an anonymous class but
        //has either a CODE or UPDATEHANDLER section.
        boolean hasInit = (name != null) || hasNamedChild(node, new String[]{CODE, UPDATEHANDLER});

        if(hasInit){
            newIndentedLine();
            if(name != null) constructorHeader(attrs);
            out.print("{");

            if((name != null) && (params != null)){
                numOfTabs = savedTabs + 1;
                initializeParamsInstanceFields(params);
            }
            if(hasNamedChild(node, CODE)){
                numOfTabs = savedTabs + 1;
                visitUntilNamedChild(node, CODE, null);
            }
            if(hasNamedChild(node, UPDATEHANDLER)){
                numOfTabs = savedTabs + 1;
                newIndentedLine();
                out.print("setUpdateHandler(");
                visitUntilNamedChild(node, UPDATEHANDLER, null);
                out.print(");");
            }

            numOfTabs = savedTabs;
            newIndentedLine();
            out.print("}");
        }

        if(hasNamedChild(node, new String[]{UPDATE, ONEMIT, ONRESUME, ONSUSPEND,
                                            ONSTART, ONSTOP})){
            visitWhileNamedChild(node,
                                 new String[]{UPDATE, ONEMIT, ONRESUME, ONSUSPEND,
                                              ONSTART, ONSTOP}, null, "", 1);
        }
    }//activityBody

    //visitor for call back methods of an Activity or ThreadActivity

    private void callBack(Node node, String name){
        int savedTabs = numOfTabs;
        newIndentedLine();
        out.print("public void " + name +"(){");
        numOfTabs++;
        newIndentedLine();
        visitChildren(node);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print("}");
    }//callBack


    //class declaration

    private void classHeader(NamedNodeMap attrs){
        Node publicity = attrs.getNamedItem(ACCESS);
        if(publicity != null) publicity(publicity);
        Node className = attrs.getNamedItem(NAME);
        className(className);
        Node extnds = attrs.getNamedItem(EXTENDS);
        if(extnds != null) extnds(extnds);
        Node impls = attrs.getNamedItem(IMPLEMENTS);
        if (impls != null) impls(impls);
    }//classHeader

    //prints out the signature of the constructor.

    private void constructorHeader(NamedNodeMap attrs){
        Node className = attrs.getNamedItem(NAME);
        out.print("public " + className.getNodeValue() + "(");
        Node params = attrs.getNamedItem(PARAMS);
        if(params != null) params(params);
        out.print(")");
    }//constructorHeader

    //visitor for PUBLICITY attributes

    private void publicity(Node node){
        if( !("package".equals(node.getNodeValue())) )
            out.print(node.getNodeValue() + " ");
    }

    //visitor for NAME attributes in a class declaration

    private void className(Node node){
        out.print("class " + node.getNodeValue());
    }

    //visitor for EXTENDS attributes

    private void extnds(Node node){
        out.print(" extends " + node.getNodeValue());
    }

    //visitor for IMPLEMENTS attributes

    private void impls(Node node){
        StringTokenizer st = new StringTokenizer(node.getNodeValue());
        if(st.hasMoreTokens()){
            out.print(" implements " + st.nextToken());
            while(st.hasMoreTokens()){
                out.print(", " + st.nextToken());
            }
        }
    }//impls

    //declare the parameters as instance fields

    private void paramsAsInstanceFields(Node params){
        StringTokenizer st = new StringTokenizer(params.getNodeValue(), ",");
        while(st.hasMoreTokens()){
            newIndentedLine();
            String str = st.nextToken().trim();
            int pos = -1;
            if((pos = str.indexOf("final")) != -1) {
                String tmp = str.substring(0, pos);
                str = tmp + str.substring(pos+5);
            }
            out.println(str.trim()+";");
        }
    }//paramsAsInstanceFields

    //initialize the instance fields corresponding to the parameters

    private void initializeParamsInstanceFields(Node params){
        StringTokenizer st = new StringTokenizer(params.getNodeValue(), ",");
        while(st.hasMoreTokens()){
            StringTokenizer stt = new StringTokenizer(st.nextToken().trim(), " \t\n");
            String str = null;
            while(stt.hasMoreTokens()) str = stt.nextToken();
            newIndentedLine();
            out.println("this."+str.trim()+" = "+str.trim()+";");
        }

    }

    //
    //additional validating methods
    //

    //make sure if the class is anonymous,
    //it doesn't have IMPLEMENTS and PARAMS attributes.

    private boolean validateClassHeader(Node node){
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);
        Node impls = attrs.getNamedItem(IMPLEMENTS);
        Node params = attrs.getNamedItem(PARAMS);
        boolean valid = true;
        if(name == null){
            if(impls != null){
                valid = false;
                cat.warn("anonymous class " + node.getNodeName() +
                    " can't have implements attributes.");
            }
            if(params != null){
                valid = false;
                cat.warn("anonymous class " + node.getNodeName() +
                    " can't have params attributes.");
            }
        }
        return valid;
    }

    //check if an anonymous class declaration appears in an inappropriate context.

    private boolean validateDeclarables(Node node){
        boolean valid = true;
        Node parent = node.getParentNode();
        NamedNodeMap attrs = node.getAttributes();
        Node name = attrs.getNamedItem(NAME);
        List CAN_DECLARES = Arrays.asList(new String[]{TRIVENI, DECLARE});
        if(CAN_DECLARES.contains(parent.getNodeName()) && (name == null)){
            valid = false;
            cat.error("can't declare anonymous class " + node.getNodeName() +
                " in element " + parent.getNodeName() + ".");
        }
        return valid;
    }

    //check if an anonymous class declaration appears in an inappropriate context.

    private boolean validateActivityBody(Node node){
        boolean valid = true;
        if(hasNamedChild(node, UPDATEHANDLER) && hasNamedChild(node, UPDATE)){
            valid = false;
            cat.warn(node.getNodeName() +
                " can't have updatehandler and update element at the same time.");
        }
        return valid;
    }
    //
    //Triveni temporal Expr visitors
    //

    //<!ELEMENT ALLPAST		(%tlparam;)                              >

    public void allPast(Node node){
        tlExpr(node, "AllPast");
    }

    //<!ELEMENT AND                   ((%tlparam;), (%tlparam;))	>

    public void and(Node node){
        tlExpr(node, "And");
    }

    //<!ELEMENT BACKTO                ((%tlparam;), (%tlparam;))	>

    public void backTo(Node node){
        tlExpr(node, "BackTo");
    }

    //<!ELEMENT IMPLIES               ((%tlparam;), (%tlparam;))	>

    public void implies(Node node){
        tlExpr(node, "Implies");
    }

    //<!ELEMENT LEAF			EMPTY				>
    //<!ATTLIST LEAF
    //            LABEL               NMTOKEN                #REQUIRED  >

    public void leaf(Node node){
        out.print("new Leaf(");
        out.print(node.getAttributes().getNamedItem(LABEL).getNodeValue());
        out.print(")");
    }

    //<!ELEMENT NOT                   (%tlparam;)			>

    public void not(Node node){
        tlExpr(node, "Not");
    }

    //<!ELEMENT ONCE                  (%tlparam;)			>

    public void once(Node node){
        tlExpr(node, "Once");
    }

    //<!ELEMENT OR                    ((%tlparam;), (%tlparam;))	>

    public void or(Node node){
        tlExpr(node, "Or");
    }

    //<!ELEMENT PREVIOUS              (%tlparam;)			>

    public void previous(Node node){
        tlExpr(node, "Previous");
    }

    //<!ELEMENT SINCE                 ((%tlparam;), (%tlparam;))	>

    public void since(Node node){
        tlExpr(node, "Since");
   }

    //<!ELEMENT LABEL		      EMPTY				>
    //<!ATTLIST LABEL
    //            NAME                IDREF                  #REQUIRED  >

    public void label(Node node){
        out.print(node.getAttributes().getNamedItem(NAME).getNodeValue());
    }

    private void tlExpr(Node node, String className){
        out.print("new " + className + "(");
        int savedTabs = numOfTabs++;
        newIndentedLine();
        visitWhileNamedChild(node, TLPARAMS, null, ",", 1);
        numOfTabs = savedTabs;
        newIndentedLine();
        out.print(")");
    }


    //
    //useful methods for visiting children
    //

    void visitChildren(Node node) {
        visitChildren(node, "", 0);
    }

    /**
     * Visits all children of a node and inserts a separator
     * between them.
     */

    void visitChildren(Node node, String separator, int numOfNewLines) {
        //the last argument can't be put into sepatator because println("") != print("\n")
        if (node.hasChildNodes()) {
            int savedTabs = numOfTabs;
            NodeList children = node.getChildNodes();
            int len = children.getLength();
            boolean needSeparator = children.item(0).getNodeType() == Node.ELEMENT_NODE;
            visit(children.item(0));
            for (int i = 1; i < len; ++ i) {
                if (children.item(i).getNodeType() == Node.ELEMENT_NODE) {
                    if (needSeparator) {
                        out.print(separator);
                    } else {
                        needSeparator = true;
                    }
                }
                numOfTabs = savedTabs;
                for(int j = 0; j < numOfNewLines; j++){
                    newIndentedLine();
                }
                visit(children.item(i));
            }
            numOfTabs = savedTabs;
        }
    }

    void visitUntilNamedChild(Node node, String name, DataVisitor visitor) {
        visitUntilNamedChild(node, new String[]{name}, visitor);
    }

    /**
     * Visits the children of a node up to and including the
     * named element.  Removes the visited children.
     * Non-Elments nodes are removed and visited using the DataVisitor
     * <CODE>visitor</CODE>.
     */

    void visitUntilNamedChild(Node node, String[] names, DataVisitor visitor) {
        List nameList = Arrays.asList(names);
        Node curr = node.getFirstChild();
        while (curr != null && curr.getNodeType() != Node.ELEMENT_NODE) {
            visitNode(curr, visitor);
            node.removeChild(curr);
            curr = node.getFirstChild();
        }
        if (curr != null && nameList.contains(curr.getNodeName())) {
            visitNode(curr, visitor);
            node.removeChild(curr);
        }
    }

    void visitWhileNamedChild(Node node, String name, DataVisitor visitor,
                              String separator, int numOfNewLines) {
        visitWhileNamedChild(node, new String[] { name }, visitor, separator, numOfNewLines);
    }

    /**
     * Visits the children of a node up to and including
     * all consecutive occurrences of the named element.
     * Removes the visited children.
     * Non-Elments nodes are removed and visited using the DataVisitor
     * <CODE>visitor</CODE>.
     */

    void visitWhileNamedChild(Node node, String[] names, DataVisitor visitor,
                              String separator, int numOfNewLines) {
        //the last argument can't be put into sepatator because println("") != print("\n")
        int savedTabs = numOfTabs;
        boolean isFirst = true;
        List nameList = Arrays.asList(names);
        Node curr = node.getFirstChild();
        while (curr != null) {
            if (curr.getNodeType() == Node.ELEMENT_NODE && ! nameList.contains(curr.getNodeName())) {
                return;
            }
            numOfTabs = savedTabs;

            if(!isEmptyNode(curr)){
                if(!isFirst){
                    out.print(separator);
                    for(int i = 0; i < numOfNewLines; i++){
                        newIndentedLine();
                    }
                } else{//isFirst
                    isFirst = false;
                }

                visitNode(curr, visitor);
            }

            node.removeChild(curr);
            curr = node.getFirstChild();
        }
    }

    private int numOfNonEmptyChildren(Node node){
        int count = 0;
        NodeList children = node.getChildNodes();
        for(int i = 0; i < children.getLength(); i++){
            if(!isEmptyNode(children.item(i))) count++;
        }
        return count;
    }

    private boolean isEmptyNode(Node node){
        if(node.getNodeType() != Node.ELEMENT_NODE){
            return node.getNodeValue().trim().length() == 0;
        } else return false;
    }

    private void visitNode(Node node, DataVisitor visitor){
        if(node.getNodeType() != Node.ELEMENT_NODE){
            if(node.getNodeValue().trim().length() != 0){
                if(visitor != null) visitor.visitData(node);
            }
        } else {//Node.ELEMENT_NODE
            visit(node);
        }
    }

    void visitWhileNotNamedChild(Node node, String name, DataVisitor visitor,
                                 String separator, int numOfNewLines) {
        visitWhileNotNamedChild(node, new String[] { name }, visitor, separator, numOfNewLines);
    }

    /**
     * Visits the children of a node up to but NOT including the
     * named element.  Removes the visited children.
     * Non-Elments nodes are removed and visited using the DataVisitor
     * <CODE>visitor</CODE>.
     */
    void visitWhileNotNamedChild(Node node, String[] names, DataVisitor visitor,
                                 String separator, int numOfNewLines) {
        //the last argument can't be put into sepatator because println("") != print("\n")
        int savedTabs = numOfTabs;
        boolean isFirst = true;
        List nameList = Arrays.asList(names);
        Node curr = node.getFirstChild();
        while (curr != null) {
            if (curr.getNodeType() == Node.ELEMENT_NODE && nameList.contains(curr.getNodeName())) {
                return;
            }

            numOfTabs = savedTabs;

            if(!isEmptyNode(curr)){
                if(!isFirst){
                    out.print(separator);
                    for(int i = 0; i < numOfNewLines; i++){
                        newIndentedLine();
                    }
                } else{//isFirst
                    isFirst = false;
                }

                visitNode(curr, visitor);
            }

            node.removeChild(curr);
            curr = node.getFirstChild();
        }
    }

    Node getNamedChild(Node node, String name) {
        return getNamedChild(node, new String[] { name });
    }

    /**
     * Returns first child element whose name is in the given list.
     */

    Node getNamedChild(Node node, String[] names) {
        List nameList = Arrays.asList(names);
        if (node.hasChildNodes()) {
            NodeList children = node.getChildNodes();
            for (int i = 0; i < children.getLength(); ++ i) {
                if (children.item(i).getNodeType() == Node.ELEMENT_NODE &&
                    nameList.contains(children.item(i).getNodeName())) {
                    return children.item(i);
                }
            }
        }
        return null;
    }

    boolean hasNamedChild(Node node, String[] names) {
        return getNamedChild(node, names) != null;
    }

    boolean hasNamedChild(Node node, String name) {
        return getNamedChild(node, name) != null;
    }

    boolean hasAnyNamedChild(Node node) {
        if (node.hasChildNodes()) {
            NodeList children = node.getChildNodes();
            for (int i = 0; i < children.getLength(); ++ i) {
                if (children.item(i).getNodeType() == Node.ELEMENT_NODE) {
                    return true;
                }
            }
        }
        return false;
    }

    //start a new line with indentation

    private void newIndentedLine(){
        out.println("");
        for(int i = 0; i < numOfTabs; i++) out.print("    ");
    }

}



